1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
use isotope::builder::Builder;
use isotope::ctx::ty::MapTyCtx;
use isotope::prelude::*;
use isotope::Error as IsotopeError;
use isotope_parser::ast::{Expr, Stmt};
use isotope_parser::utils::ws;
use isotope_parser::{expr, stmt};
use nom::branch::*;
use nom::bytes::complete::*;
use nom::combinator::*;
use nom::multi::*;
use nom::sequence::*;
use nom::IResult;
use rustyline::error::ReadlineError;
use rustyline::hint::{Hinter, HistoryHinter};
use rustyline::validate::{ValidationContext, ValidationResult, Validator};
use rustyline::Context;
use rustyline_derive::{Completer, Helper, Highlighter};
use thiserror::Error;
mod command;
mod helper;
pub use command::*;
pub use helper::*;
#[derive(Debug)]
pub struct Repl {
handled: usize,
builder: Builder<MapTyCtx<DisjointSetCtx>>,
}
impl Repl {
pub fn new(_cfg: ReplConfig) -> Repl {
Repl {
handled: 0,
builder: Builder::default(),
}
}
pub fn handle(&mut self, command: &Command) -> Result<(), ReplError> {
match command {
Command::Expr(e) => self.handle_expr(e)?,
Command::Stmt(s) => self.handle_stmt(s)?,
Command::Code(e) => println!("{:?}", self.parse_expr(e)?.code()),
Command::Id(e) => println!("{:?}", self.parse_expr(e)?.id()),
Command::Addr(e) => println!("{:?}", self.parse_expr(e)?.as_ptr()),
Command::Flags(e) => println!("{:?}", self.parse_expr(e)?.load_flags()),
Command::Tyck(e) => println!("{:?}", self.parse_expr(e)?.tyck(self.builder.ctx())),
}
self.handled += 1;
Ok(())
}
pub fn parse_expr(&mut self, expr: &Expr) -> Result<TermId, ReplError> {
Ok(self.builder.expr(&expr)?)
}
pub fn handle_expr(&mut self, expr: &Expr) -> Result<(), ReplError> {
let value = self
.parse_expr(expr)?
.normalized(Form::BetaEta, u64::MAX, self.builder.ctx())
.map_err(ReplError::NormalizationError)?;
println!(
"{}",
value.to_pretty_str(80, &mut isotope::ast::PartiallyTyped)?
);
Ok(())
}
pub fn handle_stmt(&mut self, statement: &Stmt) -> Result<(), ReplError> {
self.builder.stmt(&statement).map_err(ReplError::BuildError)
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
pub struct ReplConfig {}
#[derive(Debug, Clone, Error)]
pub enum ReplError {
#[error("Error building value: {0}")]
BuildError(IsotopeError),
#[error("Error normalizing value: {0}")]
NormalizationError(IsotopeError),
}
impl From<IsotopeError> for ReplError {
fn from(err: IsotopeError) -> ReplError {
ReplError::BuildError(err)
}
}